$\forall$$T$:Type, $X$:MaInterface($T$), ${\it es}$:ES.
\\[0ex]ma{-}interface{-}consistent(${\it es}$;$X$)
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. ($\uparrow$ma{-}in{-}interface(${\it es}$;$X$;$e$)) $\Rightarrow$ (ma{-}interface{-}val(${\it es}$;$X$;$e$) $\in$ ($T$ + Top)))